KindDeq  EqDecider(Knd) 

latex

Definitions	Knd, KindDeq, union-deq(A;B;a;b), product-deq(A;B;a;b), Id, IdLnk, x:A. B(x), IdLnkDeq, t  T, IdDeq
Lemmas	id-deq wf, idlnk-deq wf, product-deq wf, Id wf, IdLnk wf, union-deq wf